nLab substitution

Redirected from "substitution rule".
Contents

Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Contents

Idea

Syntactic substitution of/for variables is one of the basic operations in formal mathematics, such as in formal logic and type theories, where it is part of the structural rules.

Syntactic substitution

Substitution is usually defined as an operation on expressions (such strings of letters from an alphabet and representing terms, formulas, propositions, dependent types, etc.) containing variables.

Suppose that PP is an expression in the context of a variable x:Xx \,\colon\, X of type, and that t:Xt \colon X is an expression which has the same type as xx. Then one denotes by

P[t/x] P[t/x]

the result of substituting tt for all occurrences of xx in PP.

For example, if PP is x 2+2xy+3x^2 + 2x y + 3 and tt is (y+z)(y+z), then P[t/x]P[t/x] is (y+z) 2+2(y+z)y+3(y+z)^2 + 2(y+z)y + 3.

Remark

(substitution is a meta-operation on syntax) In this approach, substitution is an operation on syntax, not an element of syntax itself. In particular, the bracket notation [t/x][t/x] is part of “meta-syntax”, not the syntax in question.

That is, the literal string of symbols “P[t/x]P[t/x]” is not itself an expression in the language under consideration, but denotes such an expression, in the same way that “2+22+2” is not literally an integer but denotes the numeral44”.

Compare also Rem. below.

Simultaneous substitution

Substitution for multiple variables does not, in general, commute. That is, the expressions

P[t/x][s/y]andP[s/y][t/x] P[t/x][s/y] \qquad\text{and}\qquad P[s/y][t/x]

are not in general the same: The former substitutes ss for occurrences of yy in tt, but not tt for occurrences of xx in ss, while the latter has the opposite behavior. We also write

P[t,s/x,y] P[t,s/x,y]

to denote the simultaneous substitution of tt for xx and ss for yy, in which neither occurrences of xx in ss nor occurrences of yy in tt are substituted for; this is generally not the same as either iterated substitution.

Avoiding variable capture

If the language in question contains variable binders, then there is a subtlety to substitution: if tt contains free variables that are bound in PP, then we cannot simply textually substitute tt for xx and obtain an expression with the desired meaning.

For instance, if PP is y(x+y=1)\exists y (x + y = 1), and tt is the free variable yy, then a literal interpretation of P[t/x]P[t/x] would produce y(y+y=1)\exists y (y + y = 1). But PP is true (universally in its free variables) if the variables have type \mathbb{Z}, while y(y+y=1)\exists y (y + y = 1) is not. The free variable yy in tt has been “captured” by the binder y\exists y in PP.

We say that tt is substitutable for xx in PP if performing a literal textual substitution as above would not result in undesired variable capture. If tt is not substitutable for xx in PP, then we can always replace PP by an alpha-equivalent expression in which tt is substitutable for xx. Since we often consider formulas only up to α\alpha-equivalence anyway, one usually defines the notation “P[t/x]P[t/x]” to include an α\alpha-conversion of PP, if necessary, to make tt substitutable for xx.

In computer implementations of type theories, however, the issue of variable binding and capture is one of the trickiest things to get right. Performing α\alpha-conversions is difficult and tedious, and other solutions exist, such as using de Bruijn indices to represent bound variables.

As an admissible type inference rule

A general property of type theories (and other formal mathematics) is that substitution is an admissible rule.

Roughly, this means that if PP is an expression of some type, then so is the result P[t/x]P[t/x] of substitution (as long as tt and xx have the same type). This is generally not a rule “put into” the theory, but rather a property one proves about the theory; type theorists say that substitution is an admissible rule rather than a derivable rule?.

For instance, in the language of dependent type theory the following substitution rule (one of the structural rules) is an admissible rule:

(1)SubΓ,(x:A)PtypeΓ(t:A)ΓP[t/x]type. Sub \frac{ \Gamma,\; (x:A) \vdash P \;type \qquad \Gamma \vdash (t:A) }{ \Gamma \vdash P[t/x] \;type } \,.

Here “admissibility” means that if there exist derivations of Γ(t:A)\Gamma \vdash (t:A) and (x:A)Ptype(x:A) \vdash P \;type, then there also exists a derivation of ΓP[t/x]type\Gamma \vdash P[t/x] \;type. By contrast, saying that this is a derivable rule would mean that it can occur itself as part of a derivation, rather than being a meta-statement about derivations.

The substitution rule is closely related to the cut rule, and admissibility of such rules is generally proven by cut elimination.

Remark

(alternative typesetting of substitution rule)
In view of Remark we may re-express the substitution rule (1) by using actual syntactic substitutions instead of the meta-instruction “[t/x]” to perform these, if only we make explicit the variable dependency of all terms, say by a subscript:

Subγ:Γ,a γ:A γP a γtypeγ:Γt γ:Aγ:ΓP t γtype Sub \frac{ \gamma \colon \Gamma ,\;\; a_\gamma \colon A_\gamma \;\;\; \vdash \;\;\; P_{a_\gamma} \;type \;\;\;\;\;\;\;\;\;\;\; \gamma \colon \Gamma \;\;\; \vdash \;\;\; t_\gamma \colon A }{ \gamma \colon \Gamma \;\;\; \vdash \;\;\; P_{t_\gamma} \;type }

Explicit substitution

An alternative approach to substitution is to make substitution part of the object language rather than the metalanguage. That is, the notation

P[t/x]P[t/x]

is now actually itself a string of the language under consideration. One then needs reduction or equality rules describing the relationship of this string P[t/x]P[t/x] to the result of actually substituting tt for xx as in the usual approach. See explicit substitution for more details.

Categorical semantics

Definition

In the categorical semantics of type theory:

In the third case, there is a coherence issue: syntactic substitution in the usual approach is strictly associative, whereas pullback in a category is not. One way to deal with this is by using explicit substitution as described above. Another way is to strictify the category before modeling type theory; see categorical model of dependent types. For literature see (Curien-Garner-Hofmann, Lumsdaine-Warren 13).

Examples

Let 𝒞\mathcal{C} be a suitable ambient category in which we are interpreting logic/type theory.

Suppose XX and YY are types, hence interpreted as objects of 𝒞\mathcal{C}. Then a term of function type f:XYf : X \to Y is interpreted by a morphism, going by the same symbols.

Now a proposition about terms of type YY

y:YP(y) y : Y \vdash P(y)

is interpreted as an object of the slice category 𝒞 /Y\mathcal{C}_{/Y}, specifically as a (-1)-truncated object if it is to be a proposition, hence by a monomorphism

P Y. \array{ P \\ \downarrow \\ Y } \,.

For instance if 𝒞=\mathcal{C} = Set then this is the inclusion of the subset of elements of YY on which PP is true. And generally we may write

P={y:Y|isInhab(P(y))}. P = \{y : Y | isInhab(P(y)) \} \,.

Now finally the substitution of f(x)f(x) for yy in PP, hence the proposition

P(f()) X \array{ P(f(-)) \\ \downarrow \\ X }

is interpreted as the pullback

P(f()) f *P P X f Y. \array{ P(f(-)) \coloneqq & f^* P &\to& P \\ & \downarrow && \downarrow \\ & X &\stackrel{f}{\to}& Y } \,.

Notice that monomorphisms are preserved by pullback, so that this is indeed again the correct interpretation of a proposition.

Specifically, if XX is the unit type it is interpreted as a terminal object of 𝒞\mathcal{C}, and then the function ff is identified simply with a term y 0f(*)y_0 \coloneqq f(*) . In this case the substitution is evaluation of the proposition at y 0y_0, the resulting monomorphism

P(y 0) P * y 0 Y \array{ P(y_0) &\longrightarrow& P \\ \big\downarrow && \big\downarrow \\ \ast & \overset {y_0} {\longrightarrow} & Y }

over the terminal object is a truth value: the truth value of PP at y 0y_0.

type theorycategory theory
syntaxsemantics
natural deductionuniversal construction
substitution…………………….pullback of display maps
x 2:X 2A(x 2):Typex 1:X 1f(x 1):X 2x 1:X 1A(f(x 1)):Type\frac{ x_2 \colon X_2\; \vdash\; A(x_2) \colon Type \;\;\;\; x_1 \colon X_1\; \vdash \; f(x_1)\colon X_2}{ x_1 \colon X_1 \;\vdash A(f(x_1)) \colon Type}\, f *A A X 1 f X 2\array{ f^* A &\to& A \\ \downarrow && \downarrow \\ X_1 &\stackrel{f}{\to}& X_2 }

References

Discussion of the substitution rule in intuitionistic dependent type theory:

The observation that substitution forms an adjoint pair/adjoint triple with quantifiers is due to

  • Bill Lawvere, Adjointness in Foundations, (TAC), Dialectica 23 (1969), 281-296

and further developed in

  • Bill Lawvere, Equality in hyperdoctrines and

    comprehension schema as an adjoint functor_, Proceedings of the AMS Symposium on Pure Mathematics XVII (1970), 1-14.

Exposition of the interpretation of substitution as pullback:

The coherence issue involved in making this precise is discussed in

Last revised on August 27, 2024 at 13:11:03. See the history of this page for a list of all contributions to it.